0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 2 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 16 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 4368 ms)
↳12 BOUNDS(1, n^2)
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m)
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs)
computeLine#1(nil, @acc, @m) → @acc
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc))
computeLine#2(nil, @acc, @x, @xs) → nil
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n)
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs)
lineMult#1(nil, @l2, @n) → nil
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil))
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2)
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2))
matrixMult#1(nil, @m2) → nil
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
*(@x, @y) → #mult(@x, @y) [1]
+(@x, @y) → #add(@x, @y) [1]
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m) [1]
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs) [1]
computeLine#1(nil, @acc, @m) → @acc [1]
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc)) [1]
computeLine#2(nil, @acc, @x, @xs) → nil [1]
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n) [1]
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs) [1]
lineMult#1(nil, @l2, @n) → nil [1]
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) [1]
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil)) [1]
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2) [1]
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) [1]
matrixMult#1(nil, @m2) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| * => times |
| + => plus |
times(@x, @y) → #mult(@x, @y) [1]
plus(@x, @y) → #add(@x, @y) [1]
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m) [1]
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs) [1]
computeLine#1(nil, @acc, @m) → @acc [1]
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc)) [1]
computeLine#2(nil, @acc, @x, @xs) → nil [1]
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n) [1]
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs) [1]
lineMult#1(nil, @l2, @n) → nil [1]
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(plus(times(@x, @n), @y), lineMult(@n, @xs, @ys)) [1]
lineMult#2(nil, @n, @x, @xs) → ::(times(@x, @n), lineMult(@n, @xs, nil)) [1]
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2) [1]
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) [1]
matrixMult#1(nil, @m2) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
times(@x, @y) → #mult(@x, @y) [1]
plus(@x, @y) → #add(@x, @y) [1]
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m) [1]
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs) [1]
computeLine#1(nil, @acc, @m) → @acc [1]
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc)) [1]
computeLine#2(nil, @acc, @x, @xs) → nil [1]
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n) [1]
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs) [1]
lineMult#1(nil, @l2, @n) → nil [1]
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(plus(times(@x, @n), @y), lineMult(@n, @xs, @ys)) [1]
lineMult#2(nil, @n, @x, @xs) → ::(times(@x, @n), lineMult(@n, @xs, nil)) [1]
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2) [1]
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) [1]
matrixMult#1(nil, @m2) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| times :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #mult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos plus :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #add :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos computeLine :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos computeLine#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos :: :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos computeLine#2 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos nil :: :::nil:#0:#s:#neg:#pos lineMult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos lineMult#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos lineMult#2 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos matrixMult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos matrixMult#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #0 :: :::nil:#0:#s:#neg:#pos #neg :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #s :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #pred :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #pos :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #succ :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #natmult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos |
#add(v0, v1) → null_#add [0]
#mult(v0, v1) → null_#mult [0]
#natmult(v0, v1) → null_#natmult [0]
#pred(v0) → null_#pred [0]
#succ(v0) → null_#succ [0]
computeLine#1(v0, v1, v2) → null_computeLine#1 [0]
computeLine#2(v0, v1, v2, v3) → null_computeLine#2 [0]
lineMult#1(v0, v1, v2) → null_lineMult#1 [0]
lineMult#2(v0, v1, v2, v3) → null_lineMult#2 [0]
matrixMult#1(v0, v1) → null_matrixMult#1 [0]
null_#add, null_#mult, null_#natmult, null_#pred, null_#succ, null_computeLine#1, null_computeLine#2, null_lineMult#1, null_lineMult#2, null_matrixMult#1
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
nil => 1
#0 => 0
null_#add => 0
null_#mult => 0
null_#natmult => 0
null_#pred => 0
null_#succ => 0
null_computeLine#1 => 0
null_computeLine#2 => 0
null_lineMult#1 => 0
null_lineMult#2 => 0
null_matrixMult#1 => 0
#add(z, z') -{ 0 }→ @y :|: z' = @y, z = 0, @y >= 0
#add(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#add(z, z') -{ 0 }→ #succ(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #succ(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#add(z, z') -{ 0 }→ #pred(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #pred(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 1 + @y, @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: @x >= 0, z = 1 + @x, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#mult(z, z') -{ 0 }→ 1 + #natmult(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: z' = @y, z = 0, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#natmult(z, z') -{ 0 }→ #add(1 + @y, #natmult(@x, @y)) :|: @x >= 0, z = 1 + @x, z' = @y, @y >= 0
#pred(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#pred(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#pred(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#pred(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#pred(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
#succ(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#succ(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#succ(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#succ(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#succ(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
computeLine(z, z', z'') -{ 1 }→ computeLine#1(@line, @acc, @m) :|: z'' = @acc, @m >= 0, @acc >= 0, @line >= 0, z' = @m, z = @line
computeLine#1(z, z', z'') -{ 1 }→ @acc :|: z'' = @m, @acc >= 0, @m >= 0, z = 1, z' = @acc
computeLine#1(z, z', z'') -{ 1 }→ computeLine#2(@m, @acc, @x, @xs) :|: z'' = @m, @acc >= 0, @m >= 0, @x >= 0, z = 1 + @x + @xs, z' = @acc, @xs >= 0
computeLine#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
computeLine#2(z, z', z'', z1) -{ 1 }→ computeLine(@xs, @ls, lineMult(@x, @l, @acc)) :|: z = 1 + @l + @ls, @ls >= 0, @l >= 0, @acc >= 0, @x >= 0, z1 = @xs, z' = @acc, @xs >= 0, z'' = @x
computeLine#2(z, z', z'', z1) -{ 1 }→ 1 :|: @acc >= 0, @x >= 0, z = 1, z1 = @xs, z' = @acc, @xs >= 0, z'' = @x
computeLine#2(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
lineMult(z, z', z'') -{ 1 }→ lineMult#1(@l1, @l2, @n) :|: @l1 >= 0, z'' = @l2, @n >= 0, @l2 >= 0, z = @n, z' = @l1
lineMult#1(z, z', z'') -{ 1 }→ lineMult#2(@l2, @n, @x, @xs) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, z'' = @n, @l2 >= 0, @n >= 0, @xs >= 0
lineMult#1(z, z', z'') -{ 1 }→ 1 :|: z' = @l2, z'' = @n, z = 1, @l2 >= 0, @n >= 0
lineMult#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
lineMult#2(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
lineMult#2(z, z', z'', z1) -{ 1 }→ 1 + times(@x, @n) + lineMult(@n, @xs, 1) :|: z' = @n, @x >= 0, z = 1, @n >= 0, z1 = @xs, @xs >= 0, z'' = @x
lineMult#2(z, z', z'', z1) -{ 1 }→ 1 + plus(times(@x, @n), @y) + lineMult(@n, @xs, @ys) :|: z = 1 + @y + @ys, z' = @n, @x >= 0, @n >= 0, z1 = @xs, @xs >= 0, z'' = @x, @y >= 0, @ys >= 0
matrixMult(z, z') -{ 1 }→ matrixMult#1(@m1, @m2) :|: @m1 >= 0, @m2 >= 0, z = @m1, z' = @m2
matrixMult#1(z, z') -{ 1 }→ 1 :|: @m2 >= 0, z = 1, z' = @m2
matrixMult#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
matrixMult#1(z, z') -{ 1 }→ 1 + computeLine(@l, @m2, 1) + matrixMult(@ls, @m2) :|: z = 1 + @l + @ls, @ls >= 0, @l >= 0, @m2 >= 0, z' = @m2
plus(z, z') -{ 1 }→ #add(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
times(z, z') -{ 1 }→ #mult(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
| eq(start(V, V1, V6, V16),0,[times(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[computeLine(V, V1, V6, Out)],[V >= 0,V1 >= 0,V6 >= 0]). eq(start(V, V1, V6, V16),0,[fun2(V, V1, V6, Out)],[V >= 0,V1 >= 0,V6 >= 0]). eq(start(V, V1, V6, V16),0,[fun3(V, V1, V6, V16, Out)],[V >= 0,V1 >= 0,V6 >= 0,V16 >= 0]). eq(start(V, V1, V6, V16),0,[lineMult(V, V1, V6, Out)],[V >= 0,V1 >= 0,V6 >= 0]). eq(start(V, V1, V6, V16),0,[fun4(V, V1, V6, Out)],[V >= 0,V1 >= 0,V6 >= 0]). eq(start(V, V1, V6, V16),0,[fun5(V, V1, V6, V16, Out)],[V >= 0,V1 >= 0,V6 >= 0,V16 >= 0]). eq(start(V, V1, V6, V16),0,[matrixMult(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[fun6(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[fun9(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V6, V16),0,[fun7(V, Out)],[V >= 0]). eq(start(V, V1, V6, V16),0,[fun8(V, Out)],[V >= 0]). eq(times(V, V1, Out),1,[fun(V2, V3, Ret)],[Out = Ret,V = V2,V2 >= 0,V1 = V3,V3 >= 0]). eq(plus(V, V1, Out),1,[fun1(V4, V5, Ret1)],[Out = Ret1,V = V4,V4 >= 0,V1 = V5,V5 >= 0]). eq(computeLine(V, V1, V6, Out),1,[fun2(V7, V8, V9, Ret2)],[Out = Ret2,V6 = V8,V9 >= 0,V8 >= 0,V7 >= 0,V1 = V9,V = V7]). eq(fun2(V, V1, V6, Out),1,[fun3(V10, V11, V12, V13, Ret3)],[Out = Ret3,V6 = V10,V11 >= 0,V10 >= 0,V12 >= 0,V = 1 + V12 + V13,V1 = V11,V13 >= 0]). eq(fun2(V, V1, V6, Out),1,[],[Out = V14,V6 = V15,V14 >= 0,V15 >= 0,V = 1,V1 = V14]). eq(fun3(V, V1, V6, V16, Out),1,[lineMult(V19, V20, V21, Ret21),computeLine(V17, V18, Ret21, Ret4)],[Out = Ret4,V = 1 + V18 + V20,V18 >= 0,V20 >= 0,V21 >= 0,V19 >= 0,V16 = V17,V1 = V21,V17 >= 0,V6 = V19]). eq(fun3(V, V1, V6, V16, Out),1,[],[Out = 1,V22 >= 0,V23 >= 0,V = 1,V16 = V24,V1 = V22,V24 >= 0,V6 = V23]). eq(lineMult(V, V1, V6, Out),1,[fun4(V25, V26, V27, Ret5)],[Out = Ret5,V25 >= 0,V6 = V26,V27 >= 0,V26 >= 0,V = V27,V1 = V25]). eq(fun4(V, V1, V6, Out),1,[fun5(V28, V29, V30, V31, Ret6)],[Out = Ret6,V1 = V28,V30 >= 0,V = 1 + V30 + V31,V6 = V29,V28 >= 0,V29 >= 0,V31 >= 0]). eq(fun4(V, V1, V6, Out),1,[],[Out = 1,V1 = V32,V6 = V33,V = 1,V32 >= 0,V33 >= 0]). eq(fun5(V, V1, V6, V16, Out),1,[times(V34, V35, Ret010),plus(Ret010, V36, Ret01),lineMult(V35, V37, V38, Ret11)],[Out = 1 + Ret01 + Ret11,V = 1 + V36 + V38,V1 = V35,V34 >= 0,V35 >= 0,V16 = V37,V37 >= 0,V6 = V34,V36 >= 0,V38 >= 0]). eq(fun5(V, V1, V6, V16, Out),1,[times(V39, V40, Ret011),lineMult(V40, V41, 1, Ret12)],[Out = 1 + Ret011 + Ret12,V1 = V40,V39 >= 0,V = 1,V40 >= 0,V16 = V41,V41 >= 0,V6 = V39]). eq(matrixMult(V, V1, Out),1,[fun6(V42, V43, Ret7)],[Out = Ret7,V42 >= 0,V43 >= 0,V = V42,V1 = V43]). eq(fun6(V, V1, Out),1,[computeLine(V44, V45, 1, Ret012),matrixMult(V46, V45, Ret13)],[Out = 1 + Ret012 + Ret13,V = 1 + V44 + V46,V46 >= 0,V44 >= 0,V45 >= 0,V1 = V45]). eq(fun6(V, V1, Out),1,[],[Out = 1,V47 >= 0,V = 1,V1 = V47]). eq(fun1(V, V1, Out),0,[],[Out = V48,V1 = V48,V = 0,V48 >= 0]). eq(fun1(V, V1, Out),0,[fun7(V49, Ret8)],[Out = Ret8,V = 2,V1 = V49,V49 >= 0]). eq(fun1(V, V1, Out),0,[fun1(1 + (1 + V50), V51, Ret0),fun7(Ret0, Ret9)],[Out = Ret9,V50 >= 0,V1 = V51,V = 3 + V50,V51 >= 0]). eq(fun1(V, V1, Out),0,[fun8(V52, Ret10)],[Out = Ret10,V = 2,V1 = V52,V52 >= 0]). eq(fun1(V, V1, Out),0,[fun1(1 + (1 + V53), V54, Ret02),fun8(Ret02, Ret14)],[Out = Ret14,V53 >= 0,V1 = V54,V = 3 + V53,V54 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 1 + V55,V55 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V56 >= 0,V = 1 + V56,V1 = 0]). eq(fun(V, V1, Out),0,[fun9(V57, V58, Ret15)],[Out = 1 + Ret15,V57 >= 0,V = 1 + V57,V1 = 1 + V58,V58 >= 0]). eq(fun9(V, V1, Out),0,[],[Out = 0,V1 = V59,V = 0,V59 >= 0]). eq(fun9(V, V1, Out),0,[fun9(V61, V60, Ret16),fun1(1 + V60, Ret16, Ret17)],[Out = Ret17,V61 >= 0,V = 1 + V61,V1 = V60,V60 >= 0]). eq(fun7(V, Out),0,[],[Out = 2,V = 0]). eq(fun7(V, Out),0,[],[Out = 3 + V62,V62 >= 0,V = 2 + V62]). eq(fun7(V, Out),0,[],[Out = 0,V = 2]). eq(fun7(V, Out),0,[],[Out = 2 + V63,V63 >= 0,V = 3 + V63]). eq(fun8(V, Out),0,[],[Out = 2,V = 0]). eq(fun8(V, Out),0,[],[Out = 0,V = 2]). eq(fun8(V, Out),0,[],[Out = 2 + V64,V64 >= 0,V = 3 + V64]). eq(fun8(V, Out),0,[],[Out = 3 + V65,V65 >= 0,V = 2 + V65]). eq(fun1(V, V1, Out),0,[],[Out = 0,V66 >= 0,V67 >= 0,V = V66,V1 = V67]). eq(fun(V, V1, Out),0,[],[Out = 0,V68 >= 0,V69 >= 0,V = V68,V1 = V69]). eq(fun9(V, V1, Out),0,[],[Out = 0,V70 >= 0,V71 >= 0,V = V70,V1 = V71]). eq(fun7(V, Out),0,[],[Out = 0,V72 >= 0,V = V72]). eq(fun8(V, Out),0,[],[Out = 0,V73 >= 0,V = V73]). eq(fun2(V, V1, V6, Out),0,[],[Out = 0,V74 >= 0,V6 = V75,V76 >= 0,V = V74,V1 = V76,V75 >= 0]). eq(fun3(V, V1, V6, V16, Out),0,[],[Out = 0,V16 = V77,V78 >= 0,V6 = V79,V80 >= 0,V = V78,V1 = V80,V79 >= 0,V77 >= 0]). eq(fun4(V, V1, V6, Out),0,[],[Out = 0,V81 >= 0,V6 = V82,V83 >= 0,V = V81,V1 = V83,V82 >= 0]). eq(fun5(V, V1, V6, V16, Out),0,[],[Out = 0,V16 = V84,V85 >= 0,V6 = V86,V87 >= 0,V = V85,V1 = V87,V86 >= 0,V84 >= 0]). eq(fun6(V, V1, Out),0,[],[Out = 0,V88 >= 0,V89 >= 0,V = V88,V1 = V89]). input_output_vars(times(V,V1,Out),[V,V1],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(computeLine(V,V1,V6,Out),[V,V1,V6],[Out]). input_output_vars(fun2(V,V1,V6,Out),[V,V1,V6],[Out]). input_output_vars(fun3(V,V1,V6,V16,Out),[V,V1,V6,V16],[Out]). input_output_vars(lineMult(V,V1,V6,Out),[V,V1,V6],[Out]). input_output_vars(fun4(V,V1,V6,Out),[V,V1,V6],[Out]). input_output_vars(fun5(V,V1,V6,V16,Out),[V,V1,V6,V16],[Out]). input_output_vars(matrixMult(V,V1,Out),[V,V1],[Out]). input_output_vars(fun6(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun9(V,V1,Out),[V,V1],[Out]). input_output_vars(fun7(V,Out),[V],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun7/2]
1. non_recursive : [fun8/2]
2. recursive [non_tail] : [fun1/3]
3. non_recursive : [plus/3]
4. recursive [non_tail] : [fun9/3]
5. non_recursive : [fun/3]
6. non_recursive : [times/3]
7. recursive : [fun4/4,fun5/5,lineMult/4]
8. recursive : [computeLine/4,fun2/4,fun3/5]
9. recursive : [fun6/3,matrixMult/3]
10. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun7/2
1. SCC is partially evaluated into fun8/2
2. SCC is partially evaluated into fun1/3
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into fun9/3
5. SCC is partially evaluated into fun/3
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into lineMult/4
8. SCC is partially evaluated into computeLine/4
9. SCC is partially evaluated into matrixMult/3
10. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun7/2
* CE 51 is refined into CE [56]
* CE 49 is refined into CE [57]
* CE 50 is refined into CE [58]
* CE 48 is refined into CE [59]
### Cost equations --> "Loop" of fun7/2
* CEs [56] --> Loop 32
* CEs [57] --> Loop 33
* CEs [58] --> Loop 34
* CEs [59] --> Loop 35
### Ranking functions of CR fun7(V,Out)
#### Partial ranking functions of CR fun7(V,Out)
### Specialization of cost equations fun8/2
* CE 54 is refined into CE [60]
* CE 55 is refined into CE [61]
* CE 53 is refined into CE [62]
* CE 52 is refined into CE [63]
### Cost equations --> "Loop" of fun8/2
* CEs [60] --> Loop 36
* CEs [61] --> Loop 37
* CEs [62] --> Loop 38
* CEs [63] --> Loop 39
### Ranking functions of CR fun8(V,Out)
#### Partial ranking functions of CR fun8(V,Out)
### Specialization of cost equations fun1/3
* CE 45 is refined into CE [64]
* CE 41 is refined into CE [65,66,67,68]
* CE 43 is refined into CE [69,70,71,72]
* CE 40 is refined into CE [73]
* CE 42 is refined into CE [74,75,76,77]
* CE 44 is refined into CE [78,79,80,81]
### Cost equations --> "Loop" of fun1/3
* CEs [76,80] --> Loop 40
* CEs [77,81] --> Loop 41
* CEs [74,78] --> Loop 42
* CEs [75,79] --> Loop 43
* CEs [68,72] --> Loop 44
* CEs [67,71] --> Loop 45
* CEs [64,66,70] --> Loop 46
* CEs [65,69] --> Loop 47
* CEs [73] --> Loop 48
### Ranking functions of CR fun1(V,V1,Out)
* RF of phase [40,41,42,43]: [V-2]
#### Partial ranking functions of CR fun1(V,V1,Out)
* Partial RF of phase [40,41,42,43]:
- RF of loop [40:1,41:1,42:1,43:1]:
V-2
### Specialization of cost equations fun9/3
* CE 46 is refined into CE [82]
* CE 47 is refined into CE [83,84,85,86,87,88,89]
### Cost equations --> "Loop" of fun9/3
* CEs [89] --> Loop 49
* CEs [88] --> Loop 50
* CEs [86] --> Loop 51
* CEs [87] --> Loop 52
* CEs [84] --> Loop 53
* CEs [85] --> Loop 54
* CEs [83] --> Loop 55
* CEs [82] --> Loop 56
### Ranking functions of CR fun9(V,V1,Out)
* RF of phase [49,50,51,52,53,54,55]: [V]
#### Partial ranking functions of CR fun9(V,V1,Out)
* Partial RF of phase [49,50,51,52,53,54,55]:
- RF of loop [49:1,50:1,51:1,52:1,53:1,54:1,55:1]:
V
### Specialization of cost equations fun/3
* CE 39 is refined into CE [90,91]
* CE 38 is refined into CE [92]
* CE 36 is refined into CE [93]
* CE 37 is refined into CE [94]
### Cost equations --> "Loop" of fun/3
* CEs [91] --> Loop 57
* CEs [90] --> Loop 58
* CEs [92] --> Loop 59
* CEs [93,94] --> Loop 60
### Ranking functions of CR fun(V,V1,Out)
#### Partial ranking functions of CR fun(V,V1,Out)
### Specialization of cost equations lineMult/4
* CE 31 is refined into CE [95]
* CE 34 is refined into CE [96]
* CE 35 is refined into CE [97]
* CE 33 is refined into CE [98,99,100,101,102,103,104,105,106,107]
* CE 32 is refined into CE [108,109,110]
### Cost equations --> "Loop" of lineMult/4
* CEs [102] --> Loop 61
* CEs [98] --> Loop 62
* CEs [103] --> Loop 63
* CEs [99,100,105] --> Loop 64
* CEs [101,104,106,107] --> Loop 65
* CEs [110] --> Loop 66
* CEs [109] --> Loop 67
* CEs [108] --> Loop 68
* CEs [95,96] --> Loop 69
* CEs [97] --> Loop 70
### Ranking functions of CR lineMult(V,V1,V6,Out)
* RF of phase [61,62,63,64,65,66,67,68]: [V1]
#### Partial ranking functions of CR lineMult(V,V1,V6,Out)
* Partial RF of phase [61,62,63,64,65,66,67,68]:
- RF of loop [61:1]:
V6/3-2/3
- RF of loop [61:1,63:1,65:1,66:1]:
V1/3-2/3
- RF of loop [62:1,64:1,65:1]:
V6
- RF of loop [62:1,64:1,68:1]:
V1
- RF of loop [63:1]:
V6/4-3/4
- RF of loop [67:1]:
V1/2-1/2
### Specialization of cost equations computeLine/4
* CE 23 is refined into CE [111]
* CE 26 is refined into CE [112]
* CE 24 is refined into CE [113]
* CE 27 is refined into CE [114]
* CE 25 is refined into CE [115,116,117]
### Cost equations --> "Loop" of computeLine/4
* CEs [117] --> Loop 71
* CEs [115] --> Loop 72
* CEs [116] --> Loop 73
* CEs [111,112] --> Loop 74
* CEs [113] --> Loop 75
* CEs [114] --> Loop 76
### Ranking functions of CR computeLine(V,V1,V6,Out)
* RF of phase [71,72,73]: [V,V1]
#### Partial ranking functions of CR computeLine(V,V1,V6,Out)
* Partial RF of phase [71,72,73]:
- RF of loop [71:1,72:1]:
V1/2-1/2
- RF of loop [71:1,72:1,73:1]:
V
- RF of loop [73:1]:
V1
### Specialization of cost equations matrixMult/3
* CE 30 is refined into CE [118,119,120,121]
* CE 28 is refined into CE [122]
* CE 29 is refined into CE [123]
### Cost equations --> "Loop" of matrixMult/3
* CEs [122] --> Loop 77
* CEs [123] --> Loop 78
* CEs [121] --> Loop 79
* CEs [120] --> Loop 80
* CEs [118] --> Loop 81
* CEs [119] --> Loop 82
### Ranking functions of CR matrixMult(V,V1,Out)
* RF of phase [79,80,81,82]: [V]
#### Partial ranking functions of CR matrixMult(V,V1,Out)
* Partial RF of phase [79,80,81,82]:
- RF of loop [79:1]:
V/3-2/3
- RF of loop [80:1]:
V
- RF of loop [81:1]:
V-1
- RF of loop [82:1]:
V/2-1/2
### Specialization of cost equations start/4
* CE 6 is refined into CE [124]
* CE 9 is refined into CE [125,126,127,128,129,130,131,132,133]
* CE 2 is refined into CE [134]
* CE 3 is refined into CE [135]
* CE 4 is refined into CE [136,137,138,139,140,141,142,143]
* CE 5 is refined into CE [144]
* CE 7 is refined into CE [145,146,147,148,149,150,151,152,153,154,155,156]
* CE 8 is refined into CE [157,158,159,160,161,162,163,164,165,166,167,168]
* CE 10 is refined into CE [169,170,171,172,173,174,175,176,177]
* CE 11 is refined into CE [178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207]
* CE 12 is refined into CE [208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237]
* CE 13 is refined into CE [238,239,240]
* CE 14 is refined into CE [241,242,243,244,245,246,247,248]
* CE 15 is refined into CE [249,250,251,252]
* CE 16 is refined into CE [253,254,255]
* CE 17 is refined into CE [256,257]
* CE 18 is refined into CE [258,259,260,261,262,263,264,265]
* CE 19 is refined into CE [266,267,268]
* CE 20 is refined into CE [269,270]
* CE 21 is refined into CE [271,272,273,274]
* CE 22 is refined into CE [275,276,277,278]
### Cost equations --> "Loop" of start/4
* CEs [157,161,165,208,211,214,217,220,223,226,229,232,235] --> Loop 83
* CEs [146] --> Loop 84
* CEs [124] --> Loop 85
* CEs [138,139] --> Loop 86
* CEs [125,126,127,128,129,130,131,132,133,250,253] --> Loop 87
* CEs [245,262] --> Loop 88
* CEs [158] --> Loop 89
* CEs [243,244,260,261] --> Loop 90
* CEs [242,259] --> Loop 91
* CEs [135,169,170,171,172,173,174,175,176,177,249] --> Loop 92
* CEs [134,136,137,140,141,142,143,144,145,147,148,149,150,151,152,153,154,155,156,159,160,162,163,164,166,167,168,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,209,210,212,213,215,216,218,219,221,222,224,225,227,228,230,231,233,234,236,237,238,239,240,241,246,247,248,251,252,254,255,256,257,258,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278] --> Loop 93
### Ranking functions of CR start(V,V1,V6,V16)
#### Partial ranking functions of CR start(V,V1,V6,V16)
Computing Bounds
=====================================
#### Cost of chains of fun7(V,Out):
* Chain [35]: 0
with precondition: [V=0,Out=2]
* Chain [34]: 0
with precondition: [Out=0,V>=0]
* Chain [33]: 0
with precondition: [V+1=Out,V>=2]
* Chain [32]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun8(V,Out):
* Chain [39]: 0
with precondition: [V=0,Out=2]
* Chain [38]: 0
with precondition: [Out=0,V>=0]
* Chain [37]: 0
with precondition: [V+1=Out,V>=2]
* Chain [36]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun1(V,V1,Out):
* Chain [[40,41,42,43],47]: 0
with precondition: [V1=0,V>=3,Out>=0,V>=Out]
* Chain [[40,41,42,43],46]: 0
with precondition: [V>=3,V1>=0,Out>=0,V>=Out+1]
* Chain [[40,41,42,43],45]: 0
with precondition: [V>=3,V1>=2,Out>=0,V+V1>=Out+1]
* Chain [[40,41,42,43],44]: 0
with precondition: [V>=3,V1>=3,Out>=0,V+V1>=Out+3]
* Chain [48]: 0
with precondition: [V=0,V1=Out,V1>=0]
* Chain [47]: 0
with precondition: [V=2,V1=0,Out=2]
* Chain [46]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [45]: 0
with precondition: [V=2,V1+1=Out,V1>=2]
* Chain [44]: 0
with precondition: [V=2,V1=Out+1,V1>=3]
#### Cost of chains of fun9(V,V1,Out):
* Chain [[49,50,51,52,53,54,55],56]: 0
with precondition: [V>=1,V1>=0,Out>=0]
* Chain [56]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun(V,V1,Out):
* Chain [60]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [59]: 0
with precondition: [V1=0,Out=0,V>=1]
* Chain [58]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [57]: 0
with precondition: [V>=2,V1>=1,Out>=1]
#### Cost of chains of lineMult(V,V1,V6,Out):
* Chain [[61,62,63,64,65,66,67,68],70]: 5*it(61)+10*it(62)+5*it(63)+5*it(65)+4*it(66)+4*it(67)+4*it(68)+2
Such that:it(67) =< V1/2
it(63) =< V6/4
aux(12) =< V1
aux(13) =< V1/3
aux(14) =< V6
aux(15) =< V6/3
it(61) =< aux(15)
it(61) =< aux(12)
it(62) =< aux(12)
it(63) =< aux(12)
it(65) =< aux(12)
it(66) =< aux(12)
it(67) =< aux(12)
it(68) =< aux(12)
it(61) =< aux(13)
it(63) =< aux(13)
it(65) =< aux(13)
it(66) =< aux(13)
it(62) =< aux(14)
it(63) =< aux(14)
it(65) =< aux(14)
it(63) =< aux(15)
with precondition: [V>=0,V1>=2,V6>=1,Out>=2]
* Chain [[61,62,63,64,65,66,67,68],69]: 5*it(61)+10*it(62)+5*it(63)+5*it(65)+4*it(66)+4*it(67)+4*it(68)+2
Such that:it(67) =< V1/2
it(63) =< V6/4
aux(16) =< V1
aux(17) =< V1/3
aux(18) =< V6
aux(19) =< V6/3
it(61) =< aux(19)
it(61) =< aux(16)
it(62) =< aux(16)
it(63) =< aux(16)
it(65) =< aux(16)
it(66) =< aux(16)
it(67) =< aux(16)
it(68) =< aux(16)
it(61) =< aux(17)
it(63) =< aux(17)
it(65) =< aux(17)
it(66) =< aux(17)
it(62) =< aux(18)
it(63) =< aux(18)
it(65) =< aux(18)
it(63) =< aux(19)
with precondition: [V>=0,V1>=1,V6>=1,Out>=1]
* Chain [70]: 2
with precondition: [V1=1,Out=1,V>=0,V6>=0]
* Chain [69]: 2
with precondition: [Out=0,V>=0,V1>=0,V6>=0]
#### Cost of chains of computeLine(V,V1,V6,Out):
* Chain [[71,72,73],76]: 10*it(71)+5*it(73)+8*s(49)+38*s(50)+28*s(52)+2
Such that:aux(40) =< V
aux(41) =< V1
aux(42) =< V1/2
it(71) =< aux(40)
it(73) =< aux(40)
it(71) =< aux(41)
it(73) =< aux(41)
it(71) =< aux(42)
s(58) =< aux(41)* (1/3)
s(61) =< aux(41)* (1/2)
s(49) =< s(61)
s(50) =< aux(41)
s(52) =< aux(41)
s(49) =< aux(41)
s(50) =< s(58)
with precondition: [V>=2,V1>=1,V6>=0,Out>=0]
* Chain [[71,72,73],75]: 10*it(71)+5*it(73)+8*s(49)+38*s(50)+28*s(52)+3
Such that:aux(43) =< V
aux(44) =< V1
aux(45) =< V1/2
it(71) =< aux(43)
it(73) =< aux(43)
it(71) =< aux(44)
it(73) =< aux(44)
it(71) =< aux(45)
s(58) =< aux(44)* (1/3)
s(61) =< aux(44)* (1/2)
s(49) =< s(61)
s(50) =< aux(44)
s(52) =< aux(44)
s(49) =< aux(44)
s(50) =< s(58)
with precondition: [Out=1,V>=2,V1>=2,V6>=0]
* Chain [[71,72,73],74]: 10*it(71)+5*it(73)+8*s(49)+38*s(50)+28*s(52)+2
Such that:aux(46) =< V
aux(47) =< V1
aux(48) =< V1/2
it(71) =< aux(46)
it(73) =< aux(46)
it(71) =< aux(47)
it(73) =< aux(47)
it(71) =< aux(48)
s(58) =< aux(47)* (1/3)
s(61) =< aux(47)* (1/2)
s(49) =< s(61)
s(50) =< aux(47)
s(52) =< aux(47)
s(49) =< aux(47)
s(50) =< s(58)
with precondition: [Out=0,V>=1,V1>=1,V6>=0]
* Chain [76]: 2
with precondition: [V=1,V6=Out,V1>=0,V6>=0]
* Chain [75]: 3
with precondition: [V1=1,Out=1,V>=1,V6>=0]
* Chain [74]: 2
with precondition: [Out=0,V>=0,V1>=0,V6>=0]
#### Cost of chains of matrixMult(V,V1,Out):
* Chain [[79,80,81,82],78]: 5*it(79)+8*it(80)+5*it(82)+20*s(132)+10*s(133)+16*s(134)+76*s(135)+56*s(136)+10*s(142)+5*s(143)+8*s(144)+38*s(145)+28*s(146)+2
Such that:it(82) =< V/2
it(79) =< V/3
aux(52) =< V1
aux(58) =< V
it(79) =< aux(58)
it(80) =< aux(58)
it(82) =< aux(58)
aux(54) =< aux(52)
aux(53) =< it(79)*aux(52)
aux(55) =< it(80)*aux(54)
s(139) =< aux(53)* (1/2)
s(149) =< aux(55)* (1/2)
s(142) =< aux(58)
s(143) =< aux(58)
s(142) =< aux(55)
s(143) =< aux(55)
s(142) =< s(149)
s(147) =< aux(55)* (1/3)
s(144) =< s(149)
s(145) =< aux(55)
s(146) =< aux(55)
s(144) =< aux(55)
s(145) =< s(147)
s(132) =< aux(58)
s(133) =< aux(58)
s(132) =< aux(53)
s(133) =< aux(53)
s(132) =< s(139)
s(137) =< aux(53)* (1/3)
s(134) =< s(139)
s(135) =< aux(53)
s(136) =< aux(53)
s(134) =< aux(53)
s(135) =< s(137)
with precondition: [V>=2,V1>=0,Out>=2]
* Chain [[79,80,81,82],77]: 5*it(79)+8*it(80)+5*it(82)+20*s(132)+10*s(133)+16*s(134)+76*s(135)+56*s(136)+10*s(142)+5*s(143)+8*s(144)+38*s(145)+28*s(146)+1
Such that:it(82) =< V/2
it(79) =< V/3
aux(52) =< V1
aux(59) =< V
it(79) =< aux(59)
it(80) =< aux(59)
it(82) =< aux(59)
aux(54) =< aux(52)
aux(53) =< it(79)*aux(52)
aux(55) =< it(80)*aux(54)
s(139) =< aux(53)* (1/2)
s(149) =< aux(55)* (1/2)
s(142) =< aux(59)
s(143) =< aux(59)
s(142) =< aux(55)
s(143) =< aux(55)
s(142) =< s(149)
s(147) =< aux(55)* (1/3)
s(144) =< s(149)
s(145) =< aux(55)
s(146) =< aux(55)
s(144) =< aux(55)
s(145) =< s(147)
s(132) =< aux(59)
s(133) =< aux(59)
s(132) =< aux(53)
s(133) =< aux(53)
s(132) =< s(139)
s(137) =< aux(53)* (1/3)
s(134) =< s(139)
s(135) =< aux(53)
s(136) =< aux(53)
s(134) =< aux(53)
s(135) =< s(137)
with precondition: [V>=1,V1>=0,Out>=1]
* Chain [78]: 2
with precondition: [V=1,Out=1,V1>=0]
* Chain [77]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of start(V,V1,V6,V16):
* Chain [93]: 124*s(200)+108*s(201)+476*s(202)+80*s(208)+40*s(209)+64*s(211)+304*s(212)+224*s(213)+80*s(214)+40*s(215)+64*s(217)+304*s(218)+224*s(219)+90*s(223)+325*s(224)+72*s(227)+342*s(228)+260*s(229)+80*s(248)+40*s(249)+64*s(251)+304*s(252)+224*s(253)+60*s(311)+75*s(312)+72*s(315)+342*s(316)+300*s(317)+32*s(354)+20*s(355)+20*s(356)+120*s(357)+20*s(358)+16*s(359)+20*s(381)+20*s(382)+90*s(423)+245*s(424)+72*s(427)+342*s(428)+110*s(467)+110*s(468)+110*s(470)+20*s(480)+20*s(481)+80*s(655)+100*s(656)+100*s(657)+100*s(659)+80*s(660)+80*s(661)+8*s(805)+10*s(806)+10*s(807)+10*s(809)+8*s(810)+7
Such that:s(804) =< V6/4
aux(74) =< V
aux(75) =< V/2
aux(76) =< V/3
aux(77) =< V/4
aux(78) =< V1
aux(79) =< V1/2
aux(80) =< V1/3
aux(81) =< V1/4
aux(82) =< V6
aux(83) =< V6/2
aux(84) =< V6/3
aux(85) =< V16
aux(86) =< V16/2
aux(87) =< V16/3
s(200) =< aux(75)
s(201) =< aux(76)
s(201) =< aux(74)
s(202) =< aux(74)
s(200) =< aux(74)
s(203) =< aux(78)
s(204) =< s(201)*aux(78)
s(205) =< s(202)*s(203)
s(206) =< s(204)* (1/2)
s(207) =< s(205)* (1/2)
s(208) =< aux(74)
s(209) =< aux(74)
s(208) =< s(205)
s(209) =< s(205)
s(208) =< s(207)
s(210) =< s(205)* (1/3)
s(211) =< s(207)
s(212) =< s(205)
s(213) =< s(205)
s(211) =< s(205)
s(212) =< s(210)
s(214) =< aux(74)
s(215) =< aux(74)
s(214) =< s(204)
s(215) =< s(204)
s(214) =< s(206)
s(216) =< s(204)* (1/3)
s(217) =< s(206)
s(218) =< s(204)
s(219) =< s(204)
s(217) =< s(204)
s(218) =< s(216)
s(223) =< aux(74)
s(224) =< aux(74)
s(223) =< aux(78)
s(224) =< aux(78)
s(223) =< aux(79)
s(225) =< aux(78)* (1/3)
s(226) =< aux(78)* (1/2)
s(227) =< s(226)
s(228) =< aux(78)
s(229) =< aux(78)
s(227) =< aux(78)
s(228) =< s(225)
s(311) =< aux(74)
s(312) =< aux(74)
s(311) =< aux(82)
s(312) =< aux(82)
s(311) =< aux(83)
s(313) =< aux(82)* (1/3)
s(314) =< aux(82)* (1/2)
s(315) =< s(314)
s(316) =< aux(82)
s(317) =< aux(82)
s(315) =< aux(82)
s(316) =< s(313)
s(354) =< aux(83)
s(381) =< aux(81)
s(382) =< aux(80)
s(382) =< aux(82)
s(357) =< aux(82)
s(381) =< aux(82)
s(354) =< aux(82)
s(357) =< aux(78)
s(381) =< aux(78)
s(381) =< aux(80)
s(423) =< aux(85)
s(424) =< aux(85)
s(423) =< aux(74)
s(424) =< aux(74)
s(423) =< aux(75)
s(425) =< aux(74)* (1/3)
s(426) =< aux(74)* (1/2)
s(427) =< s(426)
s(428) =< aux(74)
s(427) =< aux(74)
s(428) =< s(425)
s(467) =< aux(81)
s(468) =< aux(80)
s(468) =< aux(74)
s(467) =< aux(74)
s(470) =< aux(74)
s(468) =< aux(76)
s(467) =< aux(76)
s(470) =< aux(76)
s(467) =< aux(78)
s(470) =< aux(78)
s(467) =< aux(80)
s(655) =< aux(86)
s(656) =< aux(77)
s(657) =< aux(76)
s(657) =< aux(85)
s(656) =< aux(85)
s(659) =< aux(85)
s(660) =< aux(85)
s(655) =< aux(85)
s(661) =< aux(85)
s(657) =< aux(87)
s(656) =< aux(87)
s(659) =< aux(87)
s(660) =< aux(87)
s(656) =< aux(74)
s(659) =< aux(74)
s(656) =< aux(76)
s(355) =< aux(81)
s(356) =< aux(80)
s(356) =< aux(82)
s(355) =< aux(82)
s(358) =< aux(82)
s(359) =< aux(82)
s(356) =< aux(84)
s(355) =< aux(84)
s(358) =< aux(84)
s(359) =< aux(84)
s(355) =< aux(78)
s(358) =< aux(78)
s(355) =< aux(80)
s(480) =< aux(81)
s(481) =< aux(80)
s(481) =< aux(74)
s(480) =< aux(74)
s(480) =< aux(78)
s(480) =< aux(80)
s(805) =< aux(79)
s(806) =< s(804)
s(807) =< aux(84)
s(807) =< aux(78)
s(806) =< aux(78)
s(809) =< aux(78)
s(810) =< aux(78)
s(805) =< aux(78)
s(807) =< aux(80)
s(806) =< aux(80)
s(809) =< aux(80)
s(810) =< aux(80)
s(806) =< aux(82)
s(809) =< aux(82)
s(806) =< aux(84)
s(238) =< s(202)*aux(78)
s(240) =< s(238)* (1/2)
s(248) =< aux(74)
s(249) =< aux(74)
s(248) =< s(238)
s(249) =< s(238)
s(248) =< s(240)
s(250) =< s(238)* (1/3)
s(251) =< s(240)
s(252) =< s(238)
s(253) =< s(238)
s(251) =< s(238)
s(252) =< s(250)
with precondition: [V>=0]
* Chain [92]: 24*s(842)+30*s(843)+30*s(844)+60*s(845)+30*s(846)+24*s(847)+24*s(848)+4
Such that:aux(88) =< 1
aux(89) =< 1/3
aux(90) =< 1/4
aux(91) =< V16
aux(92) =< V16/2
aux(93) =< V16/3
s(842) =< aux(92)
s(843) =< aux(90)
s(844) =< aux(89)
s(844) =< aux(91)
s(845) =< aux(91)
s(843) =< aux(91)
s(846) =< aux(91)
s(847) =< aux(91)
s(842) =< aux(91)
s(848) =< aux(91)
s(844) =< aux(93)
s(843) =< aux(93)
s(846) =< aux(93)
s(847) =< aux(93)
s(845) =< aux(88)
s(843) =< aux(88)
s(846) =< aux(88)
s(843) =< aux(89)
with precondition: [V=1,V1>=0]
* Chain [91]: 1
with precondition: [V=2,V1=0]
* Chain [90]: 1
with precondition: [V=2,V1>=2]
* Chain [89]: 6
with precondition: [V=3,V1>=0,V6>=0,V16>=1]
* Chain [88]: 1
with precondition: [V1=0,V>=3]
* Chain [87]: 24*s(881)+30*s(882)+30*s(883)+60*s(884)+30*s(885)+24*s(886)+24*s(887)+5
Such that:aux(94) =< 1
aux(95) =< 1/3
aux(96) =< 1/4
aux(97) =< V
aux(98) =< V/2
aux(99) =< V/3
s(881) =< aux(98)
s(882) =< aux(96)
s(883) =< aux(95)
s(883) =< aux(97)
s(884) =< aux(97)
s(882) =< aux(97)
s(885) =< aux(97)
s(886) =< aux(97)
s(881) =< aux(97)
s(887) =< aux(97)
s(883) =< aux(99)
s(882) =< aux(99)
s(885) =< aux(99)
s(886) =< aux(99)
s(884) =< aux(94)
s(882) =< aux(94)
s(885) =< aux(94)
s(882) =< aux(95)
with precondition: [V1=1,V>=0,V6>=0]
* Chain [86]: 10*s(918)+10*s(919)+16*s(920)+20*s(926)+10*s(927)+16*s(929)+76*s(930)+56*s(931)+40*s(932)+20*s(933)+32*s(935)+152*s(936)+112*s(937)+6
Such that:s(917) =< 1
s(914) =< V
s(915) =< V/2
s(916) =< V/3
s(918) =< s(915)
s(919) =< s(916)
s(919) =< s(914)
s(920) =< s(914)
s(918) =< s(914)
s(921) =< s(917)
s(922) =< s(919)*s(917)
s(923) =< s(920)*s(921)
s(924) =< s(922)* (1/2)
s(925) =< s(923)* (1/2)
s(926) =< s(914)
s(927) =< s(914)
s(926) =< s(923)
s(927) =< s(923)
s(926) =< s(925)
s(928) =< s(923)* (1/3)
s(929) =< s(925)
s(930) =< s(923)
s(931) =< s(923)
s(929) =< s(923)
s(930) =< s(928)
s(932) =< s(914)
s(933) =< s(914)
s(932) =< s(922)
s(933) =< s(922)
s(932) =< s(924)
s(934) =< s(922)* (1/3)
s(935) =< s(924)
s(936) =< s(922)
s(937) =< s(922)
s(935) =< s(922)
s(936) =< s(934)
with precondition: [V1=1,V>=2]
* Chain [85]: 2
with precondition: [V6=1,V>=1,V1>=0]
* Chain [84]: 7
with precondition: [V6=3,V>=2,V1>=0]
* Chain [83]: 8*s(944)+10*s(945)+10*s(946)+20*s(947)+10*s(948)+8*s(949)+8*s(950)+5
Such that:s(938) =< V
s(939) =< V/2
s(940) =< V/3
s(941) =< V1
s(942) =< V1/3
s(943) =< V1/4
s(944) =< s(939)
s(945) =< s(943)
s(946) =< s(942)
s(946) =< s(938)
s(947) =< s(938)
s(945) =< s(938)
s(948) =< s(938)
s(949) =< s(938)
s(944) =< s(938)
s(950) =< s(938)
s(946) =< s(940)
s(945) =< s(940)
s(948) =< s(940)
s(949) =< s(940)
s(947) =< s(941)
s(945) =< s(941)
s(948) =< s(941)
s(945) =< s(942)
with precondition: [V16=1,V>=1,V1>=0,V6>=0]
Closed-form bounds of start(V,V1,V6,V16):
-------------------------------------
* Chain [93] with precondition: [V>=0]
- Upper bound: 1874*V+7+nat(V1)*656+nat(V1)*1120*V+V/3* (nat(V1)*560)+nat(V6)*834+nat(V16)*595+62*V+208/3*V+25*V+nat(V1/2)*8+nat(V1/3)*170+nat(V1/4)*170+nat(V6/2)*32+nat(V6/3)*10+nat(V6/4)*10+nat(V16/2)*80
- Complexity: n^2
* Chain [92] with precondition: [V=1,V1>=0]
- Upper bound: 223/2+nat(V16)*48+nat(V16/2)*24
- Complexity: n
* Chain [91] with precondition: [V=2,V1=0]
- Upper bound: 1
- Complexity: constant
* Chain [90] with precondition: [V=2,V1>=2]
- Upper bound: 1
- Complexity: constant
* Chain [89] with precondition: [V=3,V1>=0,V6>=0,V16>=1]
- Upper bound: 6
- Complexity: constant
* Chain [88] with precondition: [V1=0,V>=3]
- Upper bound: 1
- Complexity: constant
* Chain [87] with precondition: [V1=1,V>=0,V6>=0]
- Upper bound: 60*V+225/2
- Complexity: n
* Chain [86] with precondition: [V1=1,V>=2]
- Upper bound: 1043/3*V+6
- Complexity: n
* Chain [85] with precondition: [V6=1,V>=1,V1>=0]
- Upper bound: 2
- Complexity: constant
* Chain [84] with precondition: [V6=3,V>=2,V1>=0]
- Upper bound: 7
- Complexity: constant
* Chain [83] with precondition: [V16=1,V>=1,V1>=0,V6>=0]
- Upper bound: 50*V+35/6*V1+5
- Complexity: n
### Maximum cost of start(V,V1,V6,V16): max([max([6,221/2+nat(V16)*48+nat(V16/2)*24]),50*V+4+max([nat(V1/4)*10+nat(V1/3)*10,3*V+1+max([7*V+213/2,802/3*V+max([82/3*V,1628*V+1+nat(V1)*656+nat(V1)*1120*V+V/3* (nat(V1)*560)+nat(V6)*834+nat(V16)*595+57*V+25*V+nat(V1/2)*8+nat(V1/3)*170+nat(V1/4)*170+nat(V6/2)*32+nat(V6/3)*10+nat(V6/4)*10+nat(V16/2)*80])])])])+1
Asymptotic class: n^2
* Total analysis performed in 3400 ms.